World
== T:(IdIdType)
== TA:(IdIdType)
== M:(IdLnkIdType)
== (i:Id(x:IdT(i,x)))
== (i:IdAction(w-action-dec(TA;M;i)))
== (i:Id({m:Msg(M)| source(mlnk(m)) = i } List))
== (i:Idw-automaton(T(i);TA(i);M))
== Top 

latex

---

clarification:

world{i:l}
== T:(IdIdType{i})
== TA:(IdIdType{i})
== M:(IdLnkIdType{i})
== (i:Id(x:IdT(i,x)))
== (i:IdAction(w-action-dec(TA;M;i)))
== (i:Id({m:Msg(M)| source(mlnk(m)) = i  Id } List))
== (i:Idw-automaton(T(i);TA(i);M))
== Top 

latex

Definitions	IdLnk, Type, Action(dec), w-action-dec(TA;M;i), , type List, {x:A| B(x) }, Msg(M), s = t, source(l), mlnk(m), x:AB(x), x:AB(x), Id, w-automaton(T;TA;M), f(a), Top
FDL editor aliases	world